00100	
00200	CHOICE-STRATEGY-IS: 
00300	ANCESTRY∧SUPPORT[THM];
00400	
00500	EDIT-STRATEGY-IS: 
00600	DEPTH[1]∨LENGTH[5];
00700	
00800	ELAPSED-TIME =3016
00900	
01000	NIL 1 2
01100	1 ¬(cb(m,x)∧(mv(y,x,b)∧(i(y)∧(i(x)∧t(x)))));3 4
01200	2 mv(m,c,b);AXIOM
01300	3 ¬(cb(m,x)∧(t(x)∧u(x,b)));5 6
01400	4 mv(z,y,x)∧(i(z)∧(i(y)∧i(x)))⊃u(y,x)∨cl(x,f);AXIOM
01500	5 ¬(t(x)∧(u(x,b)∧o(m,x)));7 8
01600	6 cb(x,y)⊃o(x,y);AXIOM
01700	7 ¬cl(m,b);9 10
01800	8 t(y)∧(u(y,b)∧o(x,y))⊃cl(x,b);AXIOM
01900	9 ¬r(m,b);THM
02000	10 cl(x,y)∧a(x)⊃r(x,y);AXIOM